\begin{tabbing}
w{-}automaton($T$;${\it TA}$;$M$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=:($b$:Id$\rightarrow\mathbb{N}\rightarrow$($x$:Id$\rightarrow$$T$($x$))$\rightarrow$((${\it TA}$($b$)) + Unit))\+
\\[0ex]$\times$ (:($k$:Knd$\rightarrow$kindcase($k$; $a$.${\it TA}$($a$); $l$,${\it tg}$.$M$($l$,${\it tg}$) )$\rightarrow$($x$:Id$\rightarrow\mathbb{Q}\rightarrow$$T$($x$))$\rightarrow$($x$:Id$\rightarrow\mathbb{Q}\rightarrow$$T$($x$)))
\\[0ex]$\times$ ($k$:Knd$\rightarrow$kindcase($k$; $a$.${\it TA}$($a$); $l$,${\it tg}$.$M$($l$,${\it tg}$) )$\rightarrow$($x$:Id$\rightarrow$$T$($x$))$\rightarrow$(\=($l$:IdLnk\+
\\[0ex]$\times$ ($t$:Id
\\[0ex]$\times$ ($M$($l$,$t$)))) List)))
\-\-
\end{tabbing}